@${\it loc}$ effect ${\it knd}$(v:$T$)  $x$ := $f$ State(${\it ds}$) v 
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr(inr(inr(inr(inr(inl($\langle$${\it loc}$$,\,$${\it ds}$$,\,$${\it knd}$$,\,$$T$$,\,$$x$$,\,$$f$$\rangle$))))))